/*
 * To change this template, choose Tools | Templates
 * and open the template in the editor.
 */

/**
 * NuGat-API named Chameleon developed by Simon De Baets to Verimag.
 *
 */


package chameleon.model.NuGatStructure.enc;

import chameleon.gameSolver.NuGat.NuGatInterface;
import chameleon.model.NuGatStructure.bdd.Bdd;
import chameleon.model.NuGatStructure.bdd.DdManager;
import chameleon.model.NuGatStructure.utils.Expression;
import chameleon.model.NuGatStructure.utils.Node;
import chameleon.model.NuGatStructure.symbTable.SymbLayer;
import chameleon.model.NuGatStructure.symbTable.SymbTable;
import chameleon.model.NuGatStructure.utils.NodeList;
import com.sun.jna.Pointer;

/**
 * This class is a wrapper to the C struct BddEnc.
 *
 * @author simon
 */
public class BddEnc extends BaseEnc {

    public BddEnc (Pointer bddEnc, NuGatInterface  nugat){
        super (bddEnc,nugat);
    }
    
    public BddEnc (SymbTable symbTable,
                         BoolEnc bool_enc, DdManager ddManager,
                         Pointer ord_groups, NuGatInterface nugat){
        super (nugat.BddEnc_create(symbTable.ptr(), bool_enc.ptr(), ddManager.ptr(), ord_groups),
                nugat);
    }
    

    /**
     * Return the dd_mangager(CUDD) to this encoding
     * @return DdManager*
     */

    public DdManager getDdManager(){
        return new DdManager(nugat_.BddEnc_get_dd_manager(this.ptr()),nugat_);
    }

    /**
     * This function return the variables present on the layer given on parameter
     * @param SymbLayer_ptr_layer
     * @param SymbFilterType_vt
     * @return BddVarSet_ptr
     */

    public Bdd getLayerVarsCube(SymbLayer layer,
                                         int SymbFilterType_vt){
        return new Bdd (nugat_.BddEnc_get_layer_vars_cube(this.ptr(), layer.ptr(),
                SymbFilterType_vt),nugat_);
    }

    /**Function********************************************************************

       Synopsis           [Gets the support of the set of state variables]

       Description        [Returned bdd is referenced, the caller must free it after
       it is no longer used. Result is cached if not previously converted from
       internal ADD representation.  Returns NULL if an error occurred.]

       SideEffects        []

       SeeAlso            []

    ******************************************************************************/
    
    public Bdd getStateVarsCube(){
        return new Bdd(nugat_.BddEnc_get_state_vars_cube(this.ptr()),nugat_);
    }
    
    
    /**Function********************************************************************

       Synopsis           [Gets the support of the set of next-state variables]

       Description        [Returned bdd is referenced, the caller must free it after
       it is no longer used.  Result is cached if not previously converted from
       internal ADD representation. Returns NULL if an error occurred. ]

       SideEffects        []

       SeeAlso            []

    ******************************************************************************/
    
    public Bdd getNextStateVarsCube(){
        return new Bdd (nugat_.BddEnc_get_next_state_vars_cube(this.ptr()),nugat_);
    }
    
    /**
     * NuSmv description : Given a BDD whose variables are STATE variables,
   returns an isomorphic BDD where NEXT-STATE
   variables have been substituted for the
   corrisponding STATE variables
     *
     * @param bdd_ptr
     * @return bdd_ptr
     */

    public Bdd stateVarToNextStateVar( Bdd bdd){
        return new Bdd(nugat_.BddEnc_state_var_to_next_state_var(this.ptr(), bdd.ptr()),
                nugat_);
    }

    /**
     *
     * @param Expr_ptr
     * @param node_ptr_context
     * @return bdd_ptr
     */

    public Bdd exprToBdd(Expression expr,
                           Node context){
        return new Bdd (nugat_.BddEnc_expr_to_bdd(this.ptr(), expr.ptr(),
                context.ptr()),
                nugat_);
    }
    
    /**
     * 
     * @param BddEnc_ptr
     * @param bdd_ptr
     * @param NodeList_ptr_vars
     * @param do_sharing
     * @param do_indent
     * @param start_at_column
     * @param file 
     */
    
    public void printBddWff(Bdd bdd,         /* the input bdd */
                          NodeList vars,   /* variables */
                          boolean do_sharing,  /* requires dag sharing */
                          boolean do_indent,   /* requires indentation */
                          int start_at_column, /* align to column (indent only) */
                          String file            /* the stream to write to */
                          ){
        nugat_.BddEnc_print_bdd_wff(this.ptr(),
                bdd.ptr(),
                vars.ptr(),
                do_sharing,
                do_indent,
                start_at_column,
                nugat_.CmdOpenFile(file));
    }


    public Node bddToExpr(Bdd bdd){
        return new Node(nugat_.BddEnc_bdd_to_expr(this.ptr(), bdd.ptr()),nugat_);
    }

    public void forceOrder(Pointer ordGroups){
        nugat_.BddEnc_force_order(this.ptr(), ordGroups);
    }
}
